The reachability analysis of recursive programs that communicateasynchronously over reliable FIFO channels calls for restrictions to ensuredecidability. Our first result characterizes communication topologies with adecidable reachability problem restricted to eager runs (i.e., runs wheremessages are either received immediately after being sent, or never received).The problem is EXPTIME-complete in the decidable case. The second result is adoubly exponential time algorithm for bounded context analysis in this setting,together with a matching lower bound. Both results extend and improve previouswork from La Torre et al.
展开▼
